es:ES, d, b, a:E. a  b   a  d   ||[a, b]|| = ||[a, d]||    b = d 

latex

Definitions	t  T, x:A. B(x), E, Prop, [e, e'], ||as||, P  Q, e  e' , (e <loc e'), {T}, x. t(x), WellFnd{i}(A;x,y.R(x;y)), ES, A & B, P  Q, P & Q, P  Q, 1of(t), pred(e), P  Q, True, T, Top, S  T, False, A, AB, ij, (x  l)
Lemmas	le wf, member-es-interval, es-le-self, l member non nil, pos length, es-interval-eq, es-pred-one-one, length-append, top wf, squash wf, true wf, es-interval-less, es-le-pred, es-pred-locl, es-pred wf, es-le-iff, event system wf, es-locl-wellfnd, es-locl wf, es-le wf, length wf1, es-interval wf, es-E wf